(set-info :smt-lib-version 2.0)
(set-info :status sat)
(set-logic QF_NRA)
(declare-fun x () Real)
(declare-fun y () Real)
(assert (and
 (< (+ 1 (* x x) (* x y)) 0)
 (= (>= (+ x (* (- 3) y) (* 5 (* x x)) (* 5 x y)) 0)
    (>= (+ x (* 2 y) (* (- 1) (* x x)) (* (- 1) x y)) 0))))
(check-sat)
